Distributed decision models are useful in a variety of problems. One important area where distributed decision processing has seen some benefit is within an area known in the art as Boolean Satisfiability (SAT) problems. SAT problems arise in a number of arenas, but one of importance is in the field of integrated circuit design and verification. As the demand for more functional consumer electronics has increased, so has the complexity of the integrated circuits powering the consumer electronics. With the increase in the complexity of the circuit there have been significant increases in the challenges within the design and verification of these more complex circuits.
In the verification process there are a number of computerized techniques employed. For example, a common technique for verification of digital designs is known as model checking. Model checking is typically implemented with a Binary Decision Diagram (BDD). With recent advances in SAT solvers they are proving to be a reasonable alternative to BDD's in digital circuit verification. A given Boolean formula is considered satisfiable if all the variables in the formula can take on such values to make the formula evaluate to true. Alternatively, and potentially more important, if no combination of values can be found that forces the function to evaluate to true, then the formula is unsatisfiable.
SAT solvers typically require the function to be expressed in Conjunctive Normal Form (CNF) which is a conjunction of clauses, where a clause is a disjunction of literals. A literal is either a variable name or its negation. A satisfying assignment returned by the SAT solver corresponds to a counterexample of length k. If the problem is unsatisfiable at length k, the SAT returns a proof that there are no counterexamples of length less than or equal to k.
The DPLL (Davis-Putnam-Logemann-Loveland algorithm) is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e., for solving the CNF-SAT problem. The basic backtracking algorithm runs by choosing a branching literal, assigning a truth value to it, simplifying the formula, and then recursively checking if the simplified formula is satisfiable. If this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the splitting rule, as it splits the problem into two simpler sub-problems. The simplification step essentially removes all clauses which become true under the assignment from the formula, and all literals that become false from the remaining clauses.
Multiple contributions well-known by engineers knowledgeable in the field have been proposed in the literature, mainly in three directions: 1. defining different policies for choosing the branching literals; 2. defining new data structures to make the algorithm faster, especially the part on unit propagation; and 3. defining variants of the basic backtracking algorithm. The latter direction includes non-chronological backtracking and clause learning. These refinements describe a method of backtracking after reaching a conflict clause which “learns” the root causes (assignments to variables) of the conflict in order to avoid reaching the same conflict again. Intuitively, backtracking can be viewed as jumping back to the root problem in a sequence of decisions and making the opposite decision.
The following strategies are well-known by engineers knowledgeable in the field: Restarts: have been previously introduced in the literature as a way to break a sequence of bad decision by starting over at certain points in the resolution and resetting the heuristic that chooses the branching literals. Number of learned clauses per conflict: each conflict can be summarized by multiple learned clauses that avoid reaching this conflict again. Traditional algorithms have been using one of such clause per conflict. Conflict clause minimization: has been introduced in the literature and is a technique to make the learned conflict clauses as small as possible. Decision replay: has been introduced in the literature to replay decisions that were not proven bad. The intuition is to avoid discarding useful choices when a backtracking goes too far to undo the root decision problem. Database compaction: the number of clauses can grow to unmanageable sizes; database compaction discards learned clauses.
With complex digital designs, verification approaches can be significantly complex and the memory limits of a computer can be quickly reached. Therefore, there exists a need for more efficient SAT solvers.